|
Affine logic is a substructural logic whose proof theory rejects the structural rule of contraction. It can also be characterized as linear logic with weakening. The name "affine logic" is associated with linear logic, to which it differs by allowing the weakening rule. Jean-Yves Girard introduced the name as part of the geometry of interaction semantics of linear logic, which characterises linear logic in terms of linear algebra; here he alludes to affine transformations on vector spaces.〔Jean-Yves Girard, 1997. '(Affine )'. Message to the TYPES mailing list.〕 The logic predated linear logic. V. N. Grishin used this logic in 1974,〔Grishin, 1974, and later, Grishin, 1981.〕 after observing that Russell's paradox cannot be derived in a set theory without contraction, even with an unbounded comprehension axiom.〔Cf. Frederic Fitch's demonstrably consistent set theory〕 Likewise, the logic formed the basis of a decidable subtheory of predicate logic, called 'Direct logic' (Ketonen & Wehrauch, 1984; Ketonen & Bellin, 1989). Affine logic can be embedded into linear logic by rewriting the affine arrow as the linear arrow . Whereas full linear logic (i.e. propositional linear logic with multiplicatives, additives and exponentials) is undecidable, full affine logic is decidable. Affine logic forms the foundation of ludics. == Notes == 〔 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Affine logic」の詳細全文を読む スポンサード リンク
|